Search Results

Documents authored by Raskin, Jean-Francois

Found 2 Possible Name Variants:

Raskin, Jean-François

Document
Complete Volume
DOI: 10.4230/LIPIcs.CONCUR.2023
LIPIcs, Volume 279, CONCUR 2023, Complete Volume

Authors: Guillermo A. Pérez and Jean-François Raskin

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
LIPIcs, Volume 279, CONCUR 2023, Complete Volume
Cite as

34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 1-666, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Proceedings{perez_et_al:LIPIcs.CONCUR.2023,
  title =	{{LIPIcs, Volume 279, CONCUR 2023, Complete Volume}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{1--666},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023},
  URN =		{urn:nbn:de:0030-drops-189936},
  doi =		{10.4230/LIPIcs.CONCUR.2023},
  annote =	{Keywords: LIPIcs, Volume 279, CONCUR 2023, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CONCUR.2023.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Guillermo A. Pérez and Jean-François Raskin

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{perez_et_al:LIPIcs.CONCUR.2023.0,
  author =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.0},
  URN =		{urn:nbn:de:0030-drops-189942},
  doi =		{10.4230/LIPIcs.CONCUR.2023.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2023.26
Rational Verification for Nash and Subgame-Perfect Equilibria in Graph Games

Authors: Léonard Brice, Jean-François Raskin, and Marie van den Bogaard

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
We study a natural problem about rational behaviors in multiplayer non-zero-sum sequential infinite duration games played on graphs: rational verification, that consists in deciding whether all the rational answers to a given strategy satisfy some specification. We give the complexities of that problem for two major concepts of rationality: Nash equilibria and subgame-perfect equilibria, and for three major classes of payoff functions: energy, discounted-sum, and mean-payoff.
Cite as

Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. Rational Verification for Nash and Subgame-Perfect Equilibria in Graph Games. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 26:1-26:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{brice_et_al:LIPIcs.MFCS.2023.26,
  author =	{Brice, L\'{e}onard and Raskin, Jean-Fran\c{c}ois and van den Bogaard, Marie},
  title =	{{Rational Verification for Nash and Subgame-Perfect Equilibria in Graph Games}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{26:1--26:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.26},
  URN =		{urn:nbn:de:0030-drops-185608},
  doi =		{10.4230/LIPIcs.MFCS.2023.26},
  annote =	{Keywords: Games on graphs, Nash equilibria, subgame-perfect equilibria}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.33
Pareto-Rational Verification

Authors: Véronique Bruyère, Jean-François Raskin, and Clément Tamines

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
We study the rational verification problem which consists in verifying the correctness of a system executing in an environment that is assumed to behave rationally. We consider the model of rationality in which the environment only executes behaviors that are Pareto-optimal with regard to its set of objectives, given the behavior of the system (which is committed in advance of any interaction). We examine two ways of specifying this behavior, first by means of a deterministic Moore machine, and then by lifting its determinism. In the latter case the machine may embed several different behaviors for the system, and the universal rational verification problem aims at verifying that all of them are correct when the environment is rational. For parity objectives, we prove that the Pareto-rational verification problem is co-NP-complete and that its universal version is in PSPACE and both NP-hard and co-NP-hard. For Boolean Büchi objectives, the former problem is Π₂𝖯-complete and the latter is PSPACE-complete. We also study the case where the objectives are expressed using LTL formulas and show that the first problem is PSPACE-complete, and that the second is 2EXPTIME-complete. Both problems are also shown to be fixed-parameter tractable for parity and Boolean Büchi objectives.
Cite as

Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Pareto-Rational Verification. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2022.33,
  author =	{Bruy\`{e}re, V\'{e}ronique and Raskin, Jean-Fran\c{c}ois and Tamines, Cl\'{e}ment},
  title =	{{Pareto-Rational Verification}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{33:1--33:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.33},
  URN =		{urn:nbn:de:0030-drops-170968},
  doi =		{10.4230/LIPIcs.CONCUR.2022.33},
  annote =	{Keywords: Rational verification, Model-checking, Pareto-optimality, \omega-regular objectives}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.115
Strategy Synthesis for Global Window PCTL

Authors: Benjamin Bordais, Damien Busatto-Gaston, Shibashis Guha, and Jean-François Raskin

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
Given a Markov decision process (MDP) M and a formula Φ, the strategy synthesis problem asks if there exists a strategy σ s.t. the resulting Markov chain M[σ] satisfies Φ. This problem is known to be undecidable for the probabilistic temporal logic PCTL. We study a class of formulae that can be seen as a fragment of PCTL where a local, bounded horizon property is enforced all along an execution. Moreover, we allow for linear expressions in the probabilistic inequalities. This logic is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis is decidable when strategies are deterministic while the general problem is undecidable.
Cite as

Benjamin Bordais, Damien Busatto-Gaston, Shibashis Guha, and Jean-François Raskin. Strategy Synthesis for Global Window PCTL. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 115:1-115:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bordais_et_al:LIPIcs.ICALP.2022.115,
  author =	{Bordais, Benjamin and Busatto-Gaston, Damien and Guha, Shibashis and Raskin, Jean-Fran\c{c}ois},
  title =	{{Strategy Synthesis for Global Window PCTL}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{115:1--115:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.115},
  URN =		{urn:nbn:de:0030-drops-164562},
  doi =		{10.4230/LIPIcs.ICALP.2022.115},
  annote =	{Keywords: Markov decision processes, synthesis, PCTL}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.116
The Complexity of SPEs in Mean-Payoff Games

Authors: Léonard Brice, Jean-François Raskin, and Marie van den Bogaard

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
We establish that the subgame perfect equilibrium (SPE) threshold problem for mean-payoff games is NP-complete. While the SPE threshold problem was recently shown to be decidable (in doubly exponential time) and NP-hard, its exact worst case complexity was left open.
Cite as

Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. The Complexity of SPEs in Mean-Payoff Games. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 116:1-116:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{brice_et_al:LIPIcs.ICALP.2022.116,
  author =	{Brice, L\'{e}onard and Raskin, Jean-Fran\c{c}ois and van den Bogaard, Marie},
  title =	{{The Complexity of SPEs in Mean-Payoff Games}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{116:1--116:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.116},
  URN =		{urn:nbn:de:0030-drops-164574},
  doi =		{10.4230/LIPIcs.ICALP.2022.116},
  annote =	{Keywords: Games on graphs, subgame-perfect equilibria, mean-payoff objectives}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.10
On the Complexity of SPEs in Parity Games

Authors: Léonard Brice, Jean-François Raskin, and Marie van den Bogaard

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
We study the complexity of problems related to subgame-perfect equilibria (SPEs) in infinite duration non zero-sum multiplayer games played on finite graphs with parity objectives. We present new complexity results that close gaps in the literature. Our techniques are based on a recent characterization of SPEs in prefix-independent games that is grounded on the notions of requirements and negotiation, and according to which the plays supported by SPEs are exactly the plays consistent with the requirement that is the least fixed point of the negotiation function. The new results are as follows. First, checking that a given requirement is a fixed point of the negotiation function is an NP-complete problem. Second, we show that the SPE constrained existence problem is NP-complete, this problem was previously known to be ExpTime-easy and NP-hard. Third, the SPE constrained existence problem is fixed-parameter tractable when the number of players and of colors are parameters. Fourth, deciding whether some requirement is the least fixed point of the negotiation function is complete for the second level of the Boolean hierarchy. Finally, the SPE-verification problem - that is, the problem of deciding whether there exists a play supported by a SPE that satisfies some LTL formula - is PSpace-complete, this problem was known to be ExpTime-easy and PSpace-hard.
Cite as

Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. On the Complexity of SPEs in Parity Games. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{brice_et_al:LIPIcs.CSL.2022.10,
  author =	{Brice, L\'{e}onard and Raskin, Jean-Fran\c{c}ois and van den Bogaard, Marie},
  title =	{{On the Complexity of SPEs in Parity Games}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{10:1--10:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.10},
  URN =		{urn:nbn:de:0030-drops-157306},
  doi =		{10.4230/LIPIcs.CSL.2022.10},
  annote =	{Keywords: Games on graphs, subgame-perfect equilibria, parity objectives}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.8
Subgame-Perfect Equilibria in Mean-Payoff Games

Authors: Léonard Brice, Jean-François Raskin, and Marie van den Bogaard

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
In this paper, we provide an effective characterization of all the subgame-perfect equilibria in infinite duration games played on finite graphs with mean-payoff objectives. To this end, we introduce the notion of requirement, and the notion of negotiation function. We establish that the plays that are supported by SPEs are exactly those that are consistent with the least fixed point of the negotiation function. Finally, we show that the negotiation function is piecewise linear, and can be analyzed using the linear algebraic tool box. As a corollary, we prove the decidability of the SPE constrained existence problem, whose status was left open in the literature.
Cite as

Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. Subgame-Perfect Equilibria in Mean-Payoff Games. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{brice_et_al:LIPIcs.CONCUR.2021.8,
  author =	{Brice, L\'{e}onard and Raskin, Jean-Fran\c{c}ois and van den Bogaard, Marie},
  title =	{{Subgame-Perfect Equilibria in Mean-Payoff Games}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{8:1--8:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.8},
  URN =		{urn:nbn:de:0030-drops-143854},
  doi =		{10.4230/LIPIcs.CONCUR.2021.8},
  annote =	{Keywords: Games on graphs, subgame-perfect equilibria, mean-payoff objectives.}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.9
Fragility and Robustness in Mean-Payoff Adversarial Stackelberg Games

Authors: Mrudula Balachander, Shibashis Guha, and Jean-François Raskin

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
Two-player mean-payoff Stackelberg games are nonzero-sum infinite duration games played on a bi-weighted graph by Leader (Player 0) and Follower (Player 1). Such games are played sequentially: first, Leader announces her strategy, second, Follower chooses his best-response. If we cannot impose which best-response is chosen by Follower, we say that Follower, though strategic, is adversarial towards Leader. The maximal value that Leader can get in this nonzero-sum game is called the adversarial Stackelberg value (ASV) of the game. We study the robustness of strategies for Leader in these games against two types of deviations: (i) Modeling imprecision - the weights on the edges of the game arena may not be exactly correct, they may be delta-away from the right one. (ii) Sub-optimal response - Follower may play epsilon-optimal best-responses instead of perfect best-responses. First, we show that if the game is zero-sum then robustness is guaranteed while in the nonzero-sum case, optimal strategies for ASV are fragile. Second, we provide a solution concept to obtain strategies for Leader that are robust to both modeling imprecision, and as well as to the epsilon-optimal responses of Follower, and study several properties and algorithmic problems related to this solution concept.
Cite as

Mrudula Balachander, Shibashis Guha, and Jean-François Raskin. Fragility and Robustness in Mean-Payoff Adversarial Stackelberg Games. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{balachander_et_al:LIPIcs.CONCUR.2021.9,
  author =	{Balachander, Mrudula and Guha, Shibashis and Raskin, Jean-Fran\c{c}ois},
  title =	{{Fragility and Robustness in Mean-Payoff Adversarial Stackelberg Games}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{9:1--9:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.9},
  URN =		{urn:nbn:de:0030-drops-143863},
  doi =		{10.4230/LIPIcs.CONCUR.2021.9},
  annote =	{Keywords: mean-payoff, Stackelberg games, synthesis}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.27
Stackelberg-Pareto Synthesis

Authors: Véronique Bruyère, Jean-François Raskin, and Clément Tamines

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
In this paper, we study the framework of two-player Stackelberg games played on graphs in which Player 0 announces a strategy and Player 1 responds rationally with a strategy that is an optimal response. While it is usually assumed that Player 1 has a single objective, we consider here the new setting where he has several. In this context, after responding with his strategy, Player 1 gets a payoff in the form of a vector of Booleans corresponding to his satisfied objectives. Rationality of Player 1 is encoded by the fact that his response must produce a Pareto-optimal payoff given the strategy of Player 0. We study the Stackelberg-Pareto Synthesis problem which asks whether Player 0 can announce a strategy which satisfies his objective, whatever the rational response of Player 1. For games in which objectives are either all parity or all reachability objectives, we show that this problem is fixed-parameter tractable and NEXPTIME-complete. This problem is already NP-complete in the simple case of reachability objectives and graphs that are trees.
Cite as

Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Stackelberg-Pareto Synthesis. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2021.27,
  author =	{Bruy\`{e}re, V\'{e}ronique and Raskin, Jean-Fran\c{c}ois and Tamines, Cl\'{e}ment},
  title =	{{Stackelberg-Pareto Synthesis}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.27},
  URN =		{urn:nbn:de:0030-drops-144040},
  doi =		{10.4230/LIPIcs.CONCUR.2021.27},
  annote =	{Keywords: Stackelberg non-zero sum games played on graphs, synthesis, parity objectives}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.17
Weighted Transducers for Robustness Verification

Authors: Emmanuel Filiot, Nicolas Mazzocchi, Jean-François Raskin, Sriram Sankaranarayanan, and Ashutosh Trivedi

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Automata theory provides us with fundamental notions such as languages, membership, emptiness and inclusion that in turn allow us to specify and verify properties of reactive systems in a useful manner. However, these notions all yield "yes"/"no" answers that sometimes fall short of being satisfactory answers when the models being analyzed are imperfect, and the observations made are prone to errors. To address this issue, a common engineering approach is not just to verify that a system satisfies a property, but whether it does so robustly. We present notions of robustness that place a metric on words, thus providing a natural notion of distance between words. Such a metric naturally leads to a topological neighborhood of words and languages, leading to quantitative and robust versions of the membership, emptiness and inclusion problems. More generally, we consider weighted transducers to model the cost of errors. Such a transducer models neighborhoods of words by providing the cost of rewriting a word into another. The main contribution of this work is to study robustness verification problems in the context of weighted transducers. We provide algorithms for solving the robust and quantitative versions of the membership and inclusion problems while providing useful motivating case studies including approximate pattern matching problems to detect clinically relevant events in a large type-1 diabetes dataset.
Cite as

Emmanuel Filiot, Nicolas Mazzocchi, Jean-François Raskin, Sriram Sankaranarayanan, and Ashutosh Trivedi. Weighted Transducers for Robustness Verification. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 17:1-17:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.CONCUR.2020.17,
  author =	{Filiot, Emmanuel and Mazzocchi, Nicolas and Raskin, Jean-Fran\c{c}ois and Sankaranarayanan, Sriram and Trivedi, Ashutosh},
  title =	{{Weighted Transducers for Robustness Verification}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{17:1--17:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.17},
  URN =		{urn:nbn:de:0030-drops-128290},
  doi =		{10.4230/LIPIcs.CONCUR.2020.17},
  annote =	{Keywords: Weighted transducers, Quantitative verification, Fault-tolerance}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.40
Monte Carlo Tree Search Guided by Symbolic Advice for MDPs

Authors: Damien Busatto-Gaston, Debraj Chakraborty, and Jean-Francois Raskin

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
In this paper, we consider the online computation of a strategy that aims at optimizing the expected average reward in a Markov decision process. The strategy is computed with a receding horizon and using Monte Carlo tree search (MCTS). We augment the MCTS algorithm with the notion of symbolic advice, and show that its classical theoretical guarantees are maintained. Symbolic advice are used to bias the selection and simulation strategies of MCTS. We describe how to use QBF and SAT solvers to implement symbolic advice in an efficient way. We illustrate our new algorithm using the popular game Pac-Man and show that the performances of our algorithm exceed those of plain MCTS as well as the performances of human players.
Cite as

Damien Busatto-Gaston, Debraj Chakraborty, and Jean-Francois Raskin. Monte Carlo Tree Search Guided by Symbolic Advice for MDPs. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 40:1-40:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{busattogaston_et_al:LIPIcs.CONCUR.2020.40,
  author =	{Busatto-Gaston, Damien and Chakraborty, Debraj and Raskin, Jean-Francois},
  title =	{{Monte Carlo Tree Search Guided by Symbolic Advice for MDPs}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{40:1--40:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.40},
  URN =		{urn:nbn:de:0030-drops-128523},
  doi =		{10.4230/LIPIcs.CONCUR.2020.40},
  annote =	{Keywords: Markov decision process, Monte Carlo tree search, symbolic advice, simulation}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.127
The Adversarial Stackelberg Value in Quantitative Games

Authors: Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
In this paper, we study the notion of adversarial Stackelberg value for two-player non-zero sum games played on bi-weighted graphs with the mean-payoff and the discounted sum functions. The adversarial Stackelberg value of Player 0 is the largest value that Player 0 can obtain when announcing her strategy to Player 1 which in turn responds with any of his best response. For the mean-payoff function, we show that the adversarial Stackelberg value is not always achievable but ε-optimal strategies exist. We show how to compute this value and prove that the associated threshold problem is in NP. For the discounted sum payoff function, we draw a link with the target discounted sum problem which explains why the problem is difficult to solve for this payoff function. We also provide solutions to related gap problems.
Cite as

Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin. The Adversarial Stackelberg Value in Quantitative Games. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 127:1-127:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.ICALP.2020.127,
  author =	{Filiot, Emmanuel and Gentilini, Raffaella and Raskin, Jean-Fran\c{c}ois},
  title =	{{The Adversarial Stackelberg Value in Quantitative Games}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{127:1--127:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.127},
  URN =		{urn:nbn:de:0030-drops-125348},
  doi =		{10.4230/LIPIcs.ICALP.2020.127},
  annote =	{Keywords: Non-zero sum games, reactive synthesis, adversarial Stackelberg}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2019.32
Expected Window Mean-Payoff

Authors: Benjamin Bordais, Shibashis Guha, and Jean-François Raskin

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
We study the expected value of the window mean-payoff measure in Markov decision processes (MDPs) and Markov chains (MCs). The window mean-payoff measure strengthens the classical mean-payoff measure by measuring the mean-payoff over a window of bounded length that slides along an infinite path. This measure ensures better stability properties than the classical mean-payoff. Window mean-payoff has been introduced previously for two-player zero-sum games. As in the case of games, we study several variants of this definition: the measure can be defined to be prefix-independent or not, and for a fixed window length or for a window length that is left parametric. For fixed window length, we provide polynomial time algorithms for the prefix-independent version for both MDPs and MCs. When the length is left parametric, the problem of computing the expected value on MDPs is as hard as computing the mean-payoff value in two-player zero-sum games, a problem for which it is not known if it can be solved in polynomial time. For the prefix-dependent version, surprisingly, the expected window mean-payoff value cannot be computed in polynomial time unless P=PSPACE. For the parametric case and the prefix-dependent case, we manage to obtain algorithms with better complexities for MCs.
Cite as

Benjamin Bordais, Shibashis Guha, and Jean-François Raskin. Expected Window Mean-Payoff. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 32:1-32:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bordais_et_al:LIPIcs.FSTTCS.2019.32,
  author =	{Bordais, Benjamin and Guha, Shibashis and Raskin, Jean-Fran\c{c}ois},
  title =	{{Expected Window Mean-Payoff}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{32:1--32:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.32},
  URN =		{urn:nbn:de:0030-drops-115940},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.32},
  annote =	{Keywords: mean-payoff, Markov decision processes, synthesis}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.13
The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games

Authors: Thomas Brihaye, Véronique Bruyère, Aline Goeminne, Jean-François Raskin, and Marie van den Bogaard

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
We study multiplayer quantitative reachability games played on a finite directed graph, where the objective of each player is to reach his target set of vertices as quickly as possible. Instead of the well-known notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium (SPE), a refinement of NE well-suited in the framework of games played on graphs. It is known that there always exists an SPE in quantitative reachability games and that the constrained existence problem is decidable. We here prove that this problem is PSPACE-complete. To obtain this result, we propose a new algorithm that iteratively builds a set of constraints characterizing the set of SPE outcomes in quantitative reachability games. This set of constraints is obtained by iterating an operator that reinforces the constraints up to obtaining a fixpoint. With this fixpoint, the set of SPE outcomes can be represented by a finite graph of size at most exponential. A careful inspection of the computation allows us to establish PSPACE membership.
Cite as

Thomas Brihaye, Véronique Bruyère, Aline Goeminne, Jean-François Raskin, and Marie van den Bogaard. The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.CONCUR.2019.13,
  author =	{Brihaye, Thomas and Bruy\`{e}re, V\'{e}ronique and Goeminne, Aline and Raskin, Jean-Fran\c{c}ois and van den Bogaard, Marie},
  title =	{{The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{13:1--13:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.13},
  URN =		{urn:nbn:de:0030-drops-109153},
  doi =		{10.4230/LIPIcs.CONCUR.2019.13},
  annote =	{Keywords: multiplayer non-zero-sum games played on graphs, quantitative reachability objectives, subgame perfect equilibria, constrained existence problem}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.21
Energy Mean-Payoff Games

Authors: Véronique Bruyère, Quentin Hautem, Mickael Randour, and Jean-François Raskin

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
In this paper, we study one-player and two-player energy mean-payoff games. Energy mean-payoff games are games of infinite duration played on a finite graph with edges labeled by 2-dimensional weight vectors. The objective of the first player (the protagonist) is to satisfy an energy objective on the first dimension and a mean-payoff objective on the second dimension. We show that optimal strategies for the first player may require infinite memory while optimal strategies for the second player (the antagonist) do not require memory. In the one-player case (where only the first player has choices), the problem of deciding who is the winner can be solved in polynomial time while for the two-player case we show co-NP membership and we give effective constructions for the infinite-memory optimal strategies of the protagonist.
Cite as

Véronique Bruyère, Quentin Hautem, Mickael Randour, and Jean-François Raskin. Energy Mean-Payoff Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2019.21,
  author =	{Bruy\`{e}re, V\'{e}ronique and Hautem, Quentin and Randour, Mickael and Raskin, Jean-Fran\c{c}ois},
  title =	{{Energy Mean-Payoff Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{21:1--21:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.21},
  URN =		{urn:nbn:de:0030-drops-109239},
  doi =		{10.4230/LIPIcs.CONCUR.2019.21},
  annote =	{Keywords: two-player zero-sum games played on graphs, energy and mean-payoff objectives, complexity study and construction of optimal strategies}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.36
Safe and Optimal Scheduling for Hard and Soft Tasks

Authors: Gilles Geeraerts, Shibashis Guha, and Jean-François Raskin

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
We consider a stochastic scheduling problem with both hard and soft tasks on a single machine. Each task is described by a discrete probability distribution over possible execution times, and possible inter-arrival times of the job, and a fixed deadline. Soft tasks also carry a penalty cost to be paid when they miss a deadline. We ask to compute an online and non-clairvoyant scheduler (i.e. one that must take decisions without knowing the future evolution of the system) that is safe and efficient. Safety imposes that deadline of hard tasks are never violated while efficient means that we want to minimise the mean cost of missing deadlines by soft tasks. First, we show that the dynamics of such a system can be modelled as a finite Markov Decision Process (MDP). Second, we show that our scheduling problem is PP-hard and in EXPTime. Third, we report on a prototype tool that solves our scheduling problem by relying on the Storm tool to analyse the corresponding MDP. We show how antichain techniques can be used as a potential heuristic.
Cite as

Gilles Geeraerts, Shibashis Guha, and Jean-François Raskin. Safe and Optimal Scheduling for Hard and Soft Tasks. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 36:1-36:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{geeraerts_et_al:LIPIcs.FSTTCS.2018.36,
  author =	{Geeraerts, Gilles and Guha, Shibashis and Raskin, Jean-Fran\c{c}ois},
  title =	{{Safe and Optimal Scheduling for Hard and Soft Tasks}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{36:1--36:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.36},
  URN =		{urn:nbn:de:0030-drops-99352},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.36},
  annote =	{Keywords: Non-clairvoyant scheduling, hard and soft tasks, automatic synthesis, Markov decision processes}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.8
Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints

Authors: Jan Kretínský, Guillermo A. Pérez, and Jean-François Raskin

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
We formalize the problem of maximizing the mean-payoff value with high probability while satisfying a parity objective in a Markov decision process (MDP) with unknown probabilistic transition function and unknown reward function. Assuming the support of the unknown transition function and a lower bound on the minimal transition probability are known in advance, we show that in MDPs consisting of a single end component, two combinations of guarantees on the parity and mean-payoff objectives can be achieved depending on how much memory one is willing to use. (i) For all epsilon and gamma we can construct an online-learning finite-memory strategy that almost-surely satisfies the parity objective and which achieves an epsilon-optimal mean payoff with probability at least 1 - gamma. (ii) Alternatively, for all epsilon and gamma there exists an online-learning infinite-memory strategy that satisfies the parity objective surely and which achieves an epsilon-optimal mean payoff with probability at least 1 - gamma. We extend the above results to MDPs consisting of more than one end component in a natural way. Finally, we show that the aforementioned guarantees are tight, i.e. there are MDPs for which stronger combinations of the guarantees cannot be ensured.
Cite as

Jan Kretínský, Guillermo A. Pérez, and Jean-François Raskin. Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kretinsky_et_al:LIPIcs.CONCUR.2018.8,
  author =	{Kret{\'\i}nsk\'{y}, Jan and P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  title =	{{Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.8},
  URN =		{urn:nbn:de:0030-drops-95468},
  doi =		{10.4230/LIPIcs.CONCUR.2018.8},
  annote =	{Keywords: Markov decision processes, Reinforcement learning, Beyond worst case}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.29
Parameterized complexity of games with monotonically ordered omega-regular objectives

Authors: Véronique Bruyère, Quentin Hautem, and Jean-François Raskin

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
In recent years, two-player zero-sum games with multiple objectives have received a lot of interest as a model for the synthesis of complex reactive systems. In this framework, Player 1 wins if he can ensure that all objectives are satisfied against any behavior of Player 2. When this is not possible to satisfy all the objectives at once, an alternative is to use some preorder on the objectives according to which subset of objectives Player 1 wants to satisfy. For example, it is often natural to provide more significance to one objective over another, a situation that can be modelled with lexicographically ordered objectives for instance. Inspired by recent work on concurrent games with multiple omega-regular objectives by Bouyer et al., we investigate in detail turned-based games with monotonically ordered and omega-regular objectives. We study the threshold problem which asks whether player 1 can ensure a payoff greater than or equal to a given threshold w.r.t. a given monotonic preorder. As the number of objectives is usually much smaller than the size of the game graph, we provide a parametric complexity analysis and we show that our threshold problem is in FPT for all monotonic preorders and all classical types of omega-regular objectives. We also provide polynomial time algorithms for Büchi, coBüchi and explicit Muller objectives for a large subclass of monotonic preorders that includes among others the lexicographic preorder. In the particular case of lexicographic preorder, we also study the complexity of computing the values and the memory requirements of optimal strategies.
Cite as

Véronique Bruyère, Quentin Hautem, and Jean-François Raskin. Parameterized complexity of games with monotonically ordered omega-regular objectives. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2018.29,
  author =	{Bruy\`{e}re, V\'{e}ronique and Hautem, Quentin and Raskin, Jean-Fran\c{c}ois},
  title =	{{Parameterized complexity of games with monotonically ordered omega-regular objectives}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{29:1--29:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.29},
  URN =		{urn:nbn:de:0030-drops-95673},
  doi =		{10.4230/LIPIcs.CONCUR.2018.29},
  annote =	{Keywords: two-player zero-sum games played on graphs, omega-regular objectives, ordered objectives, parameterized complexity}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.10
Beyond Admissibility: Dominance Between Chains of Strategies

Authors: Nicolas Basset, Ismaël Jecker, Arno Pauly, Jean-François Raskin, and Marie Van den Bogaard

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Admissible strategies, i.e. those that are not dominated by any other strategy, are a typical rationality notion in game theory. In many classes of games this is justified by results showing that any strategy is admissible or dominated by an admissible strategy. However, in games played on finite graphs with quantitative objectives (as used for reactive synthesis), this is not the case. We consider increasing chains of strategies instead to recover a satisfactory rationality notion based on dominance in such games. We start with some order-theoretic considerations establishing sufficient criteria for this to work. We then turn our attention to generalised safety/reachability games as a particular application. We propose the notion of maximal uniform chain as the desired dominance-based rationality concept in these games. Decidability of some fundamental questions about uniform chains is established.
Cite as

Nicolas Basset, Ismaël Jecker, Arno Pauly, Jean-François Raskin, and Marie Van den Bogaard. Beyond Admissibility: Dominance Between Chains of Strategies. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{basset_et_al:LIPIcs.CSL.2018.10,
  author =	{Basset, Nicolas and Jecker, Isma\"{e}l and Pauly, Arno and Raskin, Jean-Fran\c{c}ois and Van den Bogaard, Marie},
  title =	{{Beyond Admissibility: Dominance Between Chains of Strategies}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{10:1--10:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.10},
  URN =		{urn:nbn:de:0030-drops-96774},
  doi =		{10.4230/LIPIcs.CSL.2018.10},
  annote =	{Keywords: dominated strategies, admissible strategies, games played on finite graphs, reactive synthesis, reachability games, safety games, cofinal, order theory}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.MFCS.2017
LIPIcs, Volume 83, MFCS'17, Complete Volume

Authors: Kim G. Larsen, Hans L. Bodlaender, and Jean-Francois Raskin

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
LIPIcs, Volume 83, MFCS'17, Complete Volume
Cite as

42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Proceedings{larsen_et_al:LIPIcs.MFCS.2017,
  title =	{{LIPIcs, Volume 83, MFCS'17, Complete Volume}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017},
  URN =		{urn:nbn:de:0030-drops-82073},
  doi =		{10.4230/LIPIcs.MFCS.2017},
  annote =	{Keywords: Theory of Computation}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.MFCS.2017.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Kim G. Larsen, Hans L. Bodlaender, and Jean-Francois Raskin

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{larsen_et_al:LIPIcs.MFCS.2017.0,
  author =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{0:i--0:xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.0},
  URN =		{urn:nbn:de:0030-drops-80564},
  doi =		{10.4230/LIPIcs.MFCS.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2017.2
Admissibility in Games with Imperfect Information (Invited Talk)

Authors: Romain Brenguier, Arno Pauly, Jean-François Raskin, and Ocan Sankur

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
In this invited paper, we study the concept of admissible strategies for two player win/lose infinite sequential games with imperfect information. We show that in stark contrast with the perfect information variant, admissible strategies are only guaranteed to exist when players have objectives that are closed sets. As a consequence, we also study decision problems related to the existence of admissible strategies for regular games as well as finite duration games.
Cite as

Romain Brenguier, Arno Pauly, Jean-François Raskin, and Ocan Sankur. Admissibility in Games with Imperfect Information (Invited Talk). In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{brenguier_et_al:LIPIcs.CONCUR.2017.2,
  author =	{Brenguier, Romain and Pauly, Arno and Raskin, Jean-Fran\c{c}ois and Sankur, Ocan},
  title =	{{Admissibility in Games with Imperfect Information}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{2:1--2:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.2},
  URN =		{urn:nbn:de:0030-drops-78066},
  doi =		{10.4230/LIPIcs.CONCUR.2017.2},
  annote =	{Keywords: Admissibility, non-zero sum games, reactive synthesis, imperfect infor- mation}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.121
Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes

Authors: Raphaël Berthon, Mickael Randour, and Jean-François Raskin

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
The beyond worst-case synthesis problem was introduced recently by Bruyère et al. [BFRR14]: it aims at building system controllers that provide strict worst-case performance guarantees against an antagonistic environment while ensuring higher expected performance against a stochastic model of the environment. Our work extends the framework of [Bruyère/Filiot/Randour/Raskin, STACS 2014] and follow-up papers, which focused on quantitative objectives, by addressing the case of omega-regular conditions encoded as parity objectives, a natural way to represent functional requirements of systems. We build strategies that satisfy a main parity objective on all plays, while ensuring a secondary one with sufficient probability. This setting raises new challenges in comparison to quantitative objectives, as one cannot easily mix different strategies without endangering the functional properties of the system. We establish that, for all variants of this problem, deciding the existence of a strategy lies in NP and in coNP, the same complexity class as classical parity games. Hence, our framework provides additional modeling power while staying in the same complexity class.
Cite as

Raphaël Berthon, Mickael Randour, and Jean-François Raskin. Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 121:1-121:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{berthon_et_al:LIPIcs.ICALP.2017.121,
  author =	{Berthon, Rapha\"{e}l and Randour, Mickael and Raskin, Jean-Fran\c{c}ois},
  title =	{{Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{121:1--121:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.121},
  URN =		{urn:nbn:de:0030-drops-74360},
  doi =		{10.4230/LIPIcs.ICALP.2017.121},
  annote =	{Keywords: Markov decision processes, parity objectives, beyond worst-case synthesis}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.123
Admissiblity in Concurrent Games

Authors: Nicolas Basset, Gilles Geeraerts, Jean-François Raskin, and Ocan Sankur

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
In this paper, we study the notion of admissibility for randomised strategies in concurrent games. Intuitively, an admissible strategy is one where the player plays 'as well as possible', because there is no other strategy that dominates it, i.e., that wins (almost surely) against a superset of adversarial strategies. We prove that admissible strategies always exist in concurrent games, and we characterise them precisely. Then, when the objectives of the players are omega-regular, we show how to perform assume-admissible synthesis, i.e., how to compute admissible strategies that win (almost surely) under the hypothesis that the other players play admissible strategies only.
Cite as

Nicolas Basset, Gilles Geeraerts, Jean-François Raskin, and Ocan Sankur. Admissiblity in Concurrent Games. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 123:1-123:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{basset_et_al:LIPIcs.ICALP.2017.123,
  author =	{Basset, Nicolas and Geeraerts, Gilles and Raskin, Jean-Fran\c{c}ois and Sankur, Ocan},
  title =	{{Admissiblity in Concurrent Games}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{123:1--123:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.123},
  URN =		{urn:nbn:de:0030-drops-74765},
  doi =		{10.4230/LIPIcs.ICALP.2017.123},
  annote =	{Keywords: Multi-player games, admissibility, concurrent games, randomized strategies}
}
Document
DOI: 10.4230/LIPIcs.STACS.2017.50
Minkowski Games

Authors: Stéphane Le Roux, Arno Pauly, and Jean-François Raskin

Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)

Abstract
We introduce and study Minkowski games. In these games, two players take turns to choose positions in R^d based on some rules. Variants include boundedness games, where one player wants to keep the positions bounded (while the other wants to escape to infinity), and safety games, where one player wants to stay within a given set (while the other wants to leave it). We provide some general characterizations of which player can win such games, and explore the computational complexity of the associated decision problems. A natural representation of boundedness games yields coNP-completeness, whereas the safety games are undecidable.
Cite as

Stéphane Le Roux, Arno Pauly, and Jean-François Raskin. Minkowski Games. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 50:1-50:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{leroux_et_al:LIPIcs.STACS.2017.50,
  author =	{Le Roux, St\'{e}phane and Pauly, Arno and Raskin, Jean-Fran\c{c}ois},
  title =	{{Minkowski Games}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{50:1--50:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Vollmer, Heribert and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.50},
  URN =		{urn:nbn:de:0030-drops-69849},
  doi =		{10.4230/LIPIcs.STACS.2017.50},
  annote =	{Keywords: Control in R^d, determinacy, polytopic/arbitrary, coNP-complete, undecidable}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.42
Admissibility in Quantitative Graph Games

Authors: Romain Brenguier, Guillermo A. Pérez, Jean-Francois Raskin, and Ocan Sankur

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
Admissibility has been studied for games of infinite duration with Boolean objectives. We extend here this study to games of infinite duration with quantitative objectives. First, we show that, under the assumption that optimal worst-case and cooperative strategies exist, admissible strategies are guaranteed to exist. Second, we give a characterization of admissible strategies using the notion of adversarial and cooperative values of a history, and we characterize the set of outcomes that are compatible with admissible strategies. Finally, we show how these characterizations can be used to design algorithms to decide relevant verification and synthesis problems.
Cite as

Romain Brenguier, Guillermo A. Pérez, Jean-Francois Raskin, and Ocan Sankur. Admissibility in Quantitative Graph Games. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 42:1-42:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{brenguier_et_al:LIPIcs.FSTTCS.2016.42,
  author =	{Brenguier, Romain and P\'{e}rez, Guillermo A. and Raskin, Jean-Francois and Sankur, Ocan},
  title =	{{Admissibility in Quantitative Graph Games}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{42:1--42:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.42},
  URN =		{urn:nbn:de:0030-drops-68772},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.42},
  annote =	{Keywords: Quantitative games, Verification, Reactive synthesis, Admissibility}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.30
Minimizing Regret in Discounted-Sum Games

Authors: Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
In this paper, we study the problem of minimizing regret in discounted-sum games played on weighted game graphs. We give algorithms for the general problem of computing the minimal regret of the controller (Eve) as well as several variants depending on which strategies the environment (Adam) is permitted to use. We also consider the problem of synthesizing regret-free strategies for Eve in each of these scenarios.
Cite as

Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Minimizing Regret in Discounted-Sum Games. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{hunter_et_al:LIPIcs.CSL.2016.30,
  author =	{Hunter, Paul and P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  title =	{{Minimizing Regret in Discounted-Sum Games}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{30:1--30:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.30},
  URN =		{urn:nbn:de:0030-drops-65704},
  doi =		{10.4230/LIPIcs.CSL.2016.30},
  annote =	{Keywords: Quantitative games, Regret, Verification, Synthesis, Game theory}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.11
On the Complexity of Heterogeneous Multidimensional Games

Authors: Veronique Bruyere, Quentin Hautem, and Jean-Francois Raskin

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
We study two-player zero-sum turn-based games played on multidimensional weighted graphs with heterogeneous quantitative objectives. Our objectives are defined starting from the measures Inf, Sup, LimInf, and LimSup of the weights seen along the play, as well as on the window mean-payoff (WMP) measure recently introduced in [Krishnendu,Doyen,Randour,Raskin, Inf. Comput., 2015]. Whereas multidimensional games with Boolean combinations of classical mean-payoff objectives are undecidable [Velner, FOSSACS, 2015], we show that CNF/DNF Boolean combinations for heterogeneous measures taken among {WMP, Inf, Sup, LimInf, LimSup} lead to EXPTIME-completeness with exponential memory strategies for both players. We also identify several interesting fragments with better complexities and memory requirements, and show that some of them are solvable in PTIME.
Cite as

Veronique Bruyere, Quentin Hautem, and Jean-Francois Raskin. On the Complexity of Heterogeneous Multidimensional Games. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 11:1-11:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2016.11,
  author =	{Bruyere, Veronique and Hautem, Quentin and Raskin, Jean-Francois},
  title =	{{On the Complexity of Heterogeneous Multidimensional Games}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{11:1--11:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.11},
  URN =		{urn:nbn:de:0030-drops-61618},
  doi =		{10.4230/LIPIcs.CONCUR.2016.11},
  annote =	{Keywords: wo-player zero-sum games played on graphs, quantitative objectives, multidimensional heterogeneous objectives}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.121
The Complexity of Rational Synthesis

Authors: Rodica Condurache, Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
We study the computational complexity of the cooperative and non-cooperative rational synthesis problems, as introduced by Kupferman, Vardi and co-authors. We provide tight results for most of the classical omega-regular objectives, and show how to solve those problems optimally.
Cite as

Rodica Condurache, Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin. The Complexity of Rational Synthesis. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 121:1-121:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{condurache_et_al:LIPIcs.ICALP.2016.121,
  author =	{Condurache, Rodica and Filiot, Emmanuel and Gentilini, Raffaella and Raskin, Jean-Fran\c{c}ois},
  title =	{{The Complexity of Rational Synthesis}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{121:1--121:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.121},
  URN =		{urn:nbn:de:0030-drops-62565},
  doi =		{10.4230/LIPIcs.ICALP.2016.121},
  annote =	{Keywords: Non-zero sum games, reactive synthesis, omega-regular objectives}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.504
Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability

Authors: Thomas Brihaye, Véronique Bruyère, Noémie Meunier, and Jean-Francois Raskin

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
We study n-player turn-based games played on a finite directed graph. For each play, the players have to pay a cost that they want to minimize. Instead of the well-known notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium (SPE), a refinement of NE well-suited in the framework of games played on graphs. We also study natural variants of SPE, named weak (resp. very weak) SPE, where players who deviate cannot use the full class of strategies but only a subclass with a finite number of (resp. a unique) deviation step(s). Our results are threefold. Firstly, we characterize in the form of a Folk theorem the set of all plays that are the outcome of a weak SPE. Secondly, for the class of quantitative reachability games, we prove the existence of a finite-memory SPE and provide an algorithm for computing it (only existence was known with no information regarding the memory). Moreover, we show that the existence of a constrained SPE, i.e. an SPE such that each player pays a cost less than a given constant, can be decided. The proofs rely on our Folk theorem for weak SPEs (which coincide with SPEs in the case of quantitative reachability games) and on the decidability of MSO logic on infinite words. Finally with similar techniques, we provide a second general class of games for which the existence of a (constrained) weak SPE is decidable.
Cite as

Thomas Brihaye, Véronique Bruyère, Noémie Meunier, and Jean-Francois Raskin. Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 504-518, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.CSL.2015.504,
  author =	{Brihaye, Thomas and Bruy\`{e}re, V\'{e}ronique and Meunier, No\'{e}mie and Raskin, Jean-Francois},
  title =	{{Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{504--518},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.504},
  URN =		{urn:nbn:de:0030-drops-54345},
  doi =		{10.4230/LIPIcs.CSL.2015.504},
  annote =	{Keywords: multi-player games on graphs, quantitative objectives, Nash equilibrium, subgame perfect equilibrium, quantitative reachability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.100
Assume-Admissible Synthesis

Authors: Romain Brenguier, Jean-François Raskin, and Ocan Sankur

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
In this paper, we introduce a novel rule for synthesis of reactive systems, applicable to systems made of n components which have each their own objectives. It is based on the notion of admissible strategies. We compare our novel rule with previous rules defined in the literature, and we show that contrary to the previous proposals, our rule define sets of solutions which are rectangular. This property leads to solutions which are robust and resilient. We provide algorithms with optimal complexity and also an abstraction framework.
Cite as

Romain Brenguier, Jean-François Raskin, and Ocan Sankur. Assume-Admissible Synthesis. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 100-113, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{brenguier_et_al:LIPIcs.CONCUR.2015.100,
  author =	{Brenguier, Romain and Raskin, Jean-Fran\c{c}ois and Sankur, Ocan},
  title =	{{Assume-Admissible Synthesis}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{100--113},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.100},
  URN =		{urn:nbn:de:0030-drops-53711},
  doi =		{10.4230/LIPIcs.CONCUR.2015.100},
  annote =	{Keywords: Multi-player games, controller synthesis, admissibility}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.114
Reactive Synthesis Without Regret

Authors: Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Two-player zero-sum games of infinite duration and their quantitative versions are used in verification to model the interaction between a controller (Eve) and its environment (Adam). The question usually addressed is that of the existence (and computability) of a strategy for Eve that can maximize her payoff against any strategy of Adam. In this work, we are interested in strategies of Eve that minimize her regret, i.e. strategies that minimize the difference between her actual payoff and the payoff she could have achieved if she had known the strategy of Adam in advance. We give algorithms to compute the strategies of Eve that ensure minimal regret against an adversary whose choice of strategy is (i) unrestricted, (ii) limited to positional strategies, or (iii) limited to word strategies, and show that the two last cases have natural modelling applications. We also show that our notion of regret minimization in which Adam is limited to word strategies generalizes the notion of good for games introduced by Henzinger and Piterman, and is related to the notion of determinization by pruning due to Aminof, Kupferman and Lampert.
Cite as

Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Reactive Synthesis Without Regret. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 114-127, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{hunter_et_al:LIPIcs.CONCUR.2015.114,
  author =	{Hunter, Paul and P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  title =	{{Reactive Synthesis Without Regret}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{114--127},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.114},
  URN =		{urn:nbn:de:0030-drops-53675},
  doi =		{10.4230/LIPIcs.CONCUR.2015.114},
  annote =	{Keywords: Quantitative games, regret, verification, synthesis, game theory}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.133
Finite-Valued Weighted Automata

Authors: Emmanuel Filiot, Raffaella Gentilini, and Jean-Francois Raskin

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
Any weighted automaton (WA) defines a relation from finite words to values: given an input word, its set of values is obtained as the set of values computed by each accepting run on that word. A WA is k-valued if the relation it defines has degree at most k, i.e., every set of values associated with an input word has cardinality at most k. We investigate the class of quantitative languages defined by k-valued automata, for all parameters k. We consider several measures to associate values with runs: sum, discounted-sum, and more generally values in groups. We define a general procedure which decides, given a bound k and a WA over a group, whether this automaton is k-valued. We also show that any k-valued WA over a group, under some general conditions, can be decomposed as a union of k unambiguous WA. While inclusion and equivalence are undecidable problems for arbitrary sum-automata, we show, based on this decomposition, that they are decidable for k-valued sum-automata, and k-valued discounted sum-automata over inverted integer discount factors. We finally show that the quantitative Church problem is undecidable for k-valued sum-automata, even given as finite unions of deterministic sum-automata.
Cite as

Emmanuel Filiot, Raffaella Gentilini, and Jean-Francois Raskin. Finite-Valued Weighted Automata. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 133-145, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.FSTTCS.2014.133,
  author =	{Filiot, Emmanuel and Gentilini, Raffaella and Raskin, Jean-Francois},
  title =	{{Finite-Valued Weighted Automata}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{133--145},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.133},
  URN =		{urn:nbn:de:0030-drops-48388},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.133},
  annote =	{Keywords: Nested word, Transducer, Streaming}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.365
Quantitative Games with Interval Objectives

Authors: Paul Hunter and Jean-Francois Raskin

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
Traditionally quantitative games such as mean-payoff games and discount sum games have two players - one trying to maximize the payoff, the other trying to minimize it. The associated decision problem, "Can Eve (the maximizer) achieve, for example, a positive payoff?" can be thought of as one player trying to attain a payoff in the interval (0,infinity). In this paper we consider the more general problem of determining if a player can attain a payoff in a finite union of arbitrary intervals for various payoff functions (liminf/limsup, mean-payoff, discount sum, total sum). In particular this includes the interesting exact-value problem, "Can Eve achieve a payoff of exactly (e.g.) 0?"
Cite as

Paul Hunter and Jean-Francois Raskin. Quantitative Games with Interval Objectives. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 365-377, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{hunter_et_al:LIPIcs.FSTTCS.2014.365,
  author =	{Hunter, Paul and Raskin, Jean-Francois},
  title =	{{Quantitative Games with Interval Objectives}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{365--377},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.365},
  URN =		{urn:nbn:de:0030-drops-48569},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.365},
  annote =	{Keywords: Quantitative games, Mean-payoff games, Discount sum games}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.531
Multiple-Environment Markov Decision Processes

Authors: Jean-Francois Raskin and Ocan Sankur

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We introduce Multi-Environment Markov Decision Processes (MEMDPs) which are MDPs with a set of probabilistic transition functions. The goal in an MEMDP is to synthesize a single controller strategy with guaranteed performances against all environments even though the environment is unknown a priori. While MEMDPs can be seen as a special class of partially observable MDPs, we show that several verification problems that are undecidable for partially observable MDPs, are decidable for MEMDPs and sometimes have even efficient solutions.
Cite as

Jean-Francois Raskin and Ocan Sankur. Multiple-Environment Markov Decision Processes. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 531-543, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{raskin_et_al:LIPIcs.FSTTCS.2014.531,
  author =	{Raskin, Jean-Francois and Sankur, Ocan},
  title =	{{Multiple-Environment Markov Decision Processes}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{531--543},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.531},
  URN =		{urn:nbn:de:0030-drops-48692},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.531},
  annote =	{Keywords: Markov decision processes, probabilistic systems, multiple objectives}
}
Document
DOI: 10.4230/LIPIcs.STACS.2014.199
Meet Your Expectations With Guarantees: Beyond Worst-Case Synthesis in Quantitative Games

Authors: Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin

Published in: LIPIcs, Volume 25, 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)

Abstract
Classical analysis of two-player quantitative games involves an adversary (modeling the environment of the system) which is purely antagonistic and asks for strict guarantees while Markov decision processes model systems facing a purely randomized environment: the aim is then to optimize the expected payoff, with no guarantee on individual outcomes. We introduce the beyond worst-case synthesis problem, which is to construct strategies that guarantee some quantitative requirement in the worst-case while providing an higher expected value against a particular stochastic model of the environment given as input. We consider both the mean-payoff value problem and the shortest path problem. In both cases, we show how to decide the existence of finite-memory strategies satisfying the problem and how to synthesize one if one exists. We establish algorithms and we study complexity bounds and memory requirements.
Cite as

Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin. Meet Your Expectations With Guarantees: Beyond Worst-Case Synthesis in Quantitative Games. In 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 25, pp. 199-213, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.STACS.2014.199,
  author =	{Bruy\`{e}re, V\'{e}ronique and Filiot, Emmanuel and Randour, Mickael and Raskin, Jean-Fran\c{c}ois},
  title =	{{Meet Your Expectations With Guarantees: Beyond Worst-Case Synthesis in Quantitative Games}},
  booktitle =	{31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)},
  pages =	{199--213},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-65-1},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{25},
  editor =	{Mayr, Ernst W. and Portier, Natacha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2014.199},
  URN =		{urn:nbn:de:0030-drops-44589},
  doi =		{10.4230/LIPIcs.STACS.2014.199},
  annote =	{Keywords: two-player games on graphs, Markov decision processes, quantitative objectives, synthesis, worst-case and expected value, mean-payoff, shortest path}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.505
Generalized Mean-payoff and Energy Games

Authors: Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Generalized mean-payoff and energy games replace individual weights by tuples, and the limit average (resp. running sum) of each coordinate must be (resp. remain) nonnegative. These games have applications in the synthesis of resource-bounded processes with multiple resources. We prove the finite-memory determinacy of generalized energy games and show the inter-reducibility of generalized mean-payoff and energy games for finite-memory strategies. We also improve the computational complexity for solving both classes of games with finite-memory strategies: while the previously best known upper bound was EXPSPACE, and no lower bound was known, we give an optimal coNP-complete bound. For memoryless strategies, we show that the problem of deciding the existence of a winning strategy for the protagonist is NP-complete.
Cite as

Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Generalized Mean-payoff and Energy Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 505-516, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.FSTTCS.2010.505,
  author =	{Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A. and Raskin, Jean-Fran\c{c}ois},
  title =	{{Generalized Mean-payoff and Energy Games}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{505--516},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.505},
  URN =		{urn:nbn:de:0030-drops-28484},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.505},
  annote =	{Keywords: mean-payoff games, energy games, finite memory strategies, determinacy}
}

Raskin, Jean-Francois

Document
Complete Volume
DOI: 10.4230/LIPIcs.CONCUR.2023
LIPIcs, Volume 279, CONCUR 2023, Complete Volume

Authors: Guillermo A. Pérez and Jean-François Raskin

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
LIPIcs, Volume 279, CONCUR 2023, Complete Volume
Cite as

34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 1-666, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Proceedings{perez_et_al:LIPIcs.CONCUR.2023,
  title =	{{LIPIcs, Volume 279, CONCUR 2023, Complete Volume}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{1--666},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023},
  URN =		{urn:nbn:de:0030-drops-189936},
  doi =		{10.4230/LIPIcs.CONCUR.2023},
  annote =	{Keywords: LIPIcs, Volume 279, CONCUR 2023, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CONCUR.2023.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Guillermo A. Pérez and Jean-François Raskin

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{perez_et_al:LIPIcs.CONCUR.2023.0,
  author =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.0},
  URN =		{urn:nbn:de:0030-drops-189942},
  doi =		{10.4230/LIPIcs.CONCUR.2023.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2023.26
Rational Verification for Nash and Subgame-Perfect Equilibria in Graph Games

Authors: Léonard Brice, Jean-François Raskin, and Marie van den Bogaard

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
We study a natural problem about rational behaviors in multiplayer non-zero-sum sequential infinite duration games played on graphs: rational verification, that consists in deciding whether all the rational answers to a given strategy satisfy some specification. We give the complexities of that problem for two major concepts of rationality: Nash equilibria and subgame-perfect equilibria, and for three major classes of payoff functions: energy, discounted-sum, and mean-payoff.
Cite as

Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. Rational Verification for Nash and Subgame-Perfect Equilibria in Graph Games. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 26:1-26:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{brice_et_al:LIPIcs.MFCS.2023.26,
  author =	{Brice, L\'{e}onard and Raskin, Jean-Fran\c{c}ois and van den Bogaard, Marie},
  title =	{{Rational Verification for Nash and Subgame-Perfect Equilibria in Graph Games}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{26:1--26:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.26},
  URN =		{urn:nbn:de:0030-drops-185608},
  doi =		{10.4230/LIPIcs.MFCS.2023.26},
  annote =	{Keywords: Games on graphs, Nash equilibria, subgame-perfect equilibria}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.33
Pareto-Rational Verification

Authors: Véronique Bruyère, Jean-François Raskin, and Clément Tamines

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
We study the rational verification problem which consists in verifying the correctness of a system executing in an environment that is assumed to behave rationally. We consider the model of rationality in which the environment only executes behaviors that are Pareto-optimal with regard to its set of objectives, given the behavior of the system (which is committed in advance of any interaction). We examine two ways of specifying this behavior, first by means of a deterministic Moore machine, and then by lifting its determinism. In the latter case the machine may embed several different behaviors for the system, and the universal rational verification problem aims at verifying that all of them are correct when the environment is rational. For parity objectives, we prove that the Pareto-rational verification problem is co-NP-complete and that its universal version is in PSPACE and both NP-hard and co-NP-hard. For Boolean Büchi objectives, the former problem is Π₂𝖯-complete and the latter is PSPACE-complete. We also study the case where the objectives are expressed using LTL formulas and show that the first problem is PSPACE-complete, and that the second is 2EXPTIME-complete. Both problems are also shown to be fixed-parameter tractable for parity and Boolean Büchi objectives.
Cite as

Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Pareto-Rational Verification. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2022.33,
  author =	{Bruy\`{e}re, V\'{e}ronique and Raskin, Jean-Fran\c{c}ois and Tamines, Cl\'{e}ment},
  title =	{{Pareto-Rational Verification}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{33:1--33:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.33},
  URN =		{urn:nbn:de:0030-drops-170968},
  doi =		{10.4230/LIPIcs.CONCUR.2022.33},
  annote =	{Keywords: Rational verification, Model-checking, Pareto-optimality, \omega-regular objectives}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.115
Strategy Synthesis for Global Window PCTL

Authors: Benjamin Bordais, Damien Busatto-Gaston, Shibashis Guha, and Jean-François Raskin

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
Given a Markov decision process (MDP) M and a formula Φ, the strategy synthesis problem asks if there exists a strategy σ s.t. the resulting Markov chain M[σ] satisfies Φ. This problem is known to be undecidable for the probabilistic temporal logic PCTL. We study a class of formulae that can be seen as a fragment of PCTL where a local, bounded horizon property is enforced all along an execution. Moreover, we allow for linear expressions in the probabilistic inequalities. This logic is at the frontier of decidability, depending on the type of strategies considered. In particular, strategy synthesis is decidable when strategies are deterministic while the general problem is undecidable.
Cite as

Benjamin Bordais, Damien Busatto-Gaston, Shibashis Guha, and Jean-François Raskin. Strategy Synthesis for Global Window PCTL. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 115:1-115:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bordais_et_al:LIPIcs.ICALP.2022.115,
  author =	{Bordais, Benjamin and Busatto-Gaston, Damien and Guha, Shibashis and Raskin, Jean-Fran\c{c}ois},
  title =	{{Strategy Synthesis for Global Window PCTL}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{115:1--115:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.115},
  URN =		{urn:nbn:de:0030-drops-164562},
  doi =		{10.4230/LIPIcs.ICALP.2022.115},
  annote =	{Keywords: Markov decision processes, synthesis, PCTL}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.116
The Complexity of SPEs in Mean-Payoff Games

Authors: Léonard Brice, Jean-François Raskin, and Marie van den Bogaard

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
We establish that the subgame perfect equilibrium (SPE) threshold problem for mean-payoff games is NP-complete. While the SPE threshold problem was recently shown to be decidable (in doubly exponential time) and NP-hard, its exact worst case complexity was left open.
Cite as

Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. The Complexity of SPEs in Mean-Payoff Games. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 116:1-116:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{brice_et_al:LIPIcs.ICALP.2022.116,
  author =	{Brice, L\'{e}onard and Raskin, Jean-Fran\c{c}ois and van den Bogaard, Marie},
  title =	{{The Complexity of SPEs in Mean-Payoff Games}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{116:1--116:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.116},
  URN =		{urn:nbn:de:0030-drops-164574},
  doi =		{10.4230/LIPIcs.ICALP.2022.116},
  annote =	{Keywords: Games on graphs, subgame-perfect equilibria, mean-payoff objectives}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.10
On the Complexity of SPEs in Parity Games

Authors: Léonard Brice, Jean-François Raskin, and Marie van den Bogaard

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
We study the complexity of problems related to subgame-perfect equilibria (SPEs) in infinite duration non zero-sum multiplayer games played on finite graphs with parity objectives. We present new complexity results that close gaps in the literature. Our techniques are based on a recent characterization of SPEs in prefix-independent games that is grounded on the notions of requirements and negotiation, and according to which the plays supported by SPEs are exactly the plays consistent with the requirement that is the least fixed point of the negotiation function. The new results are as follows. First, checking that a given requirement is a fixed point of the negotiation function is an NP-complete problem. Second, we show that the SPE constrained existence problem is NP-complete, this problem was previously known to be ExpTime-easy and NP-hard. Third, the SPE constrained existence problem is fixed-parameter tractable when the number of players and of colors are parameters. Fourth, deciding whether some requirement is the least fixed point of the negotiation function is complete for the second level of the Boolean hierarchy. Finally, the SPE-verification problem - that is, the problem of deciding whether there exists a play supported by a SPE that satisfies some LTL formula - is PSpace-complete, this problem was known to be ExpTime-easy and PSpace-hard.
Cite as

Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. On the Complexity of SPEs in Parity Games. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{brice_et_al:LIPIcs.CSL.2022.10,
  author =	{Brice, L\'{e}onard and Raskin, Jean-Fran\c{c}ois and van den Bogaard, Marie},
  title =	{{On the Complexity of SPEs in Parity Games}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{10:1--10:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.10},
  URN =		{urn:nbn:de:0030-drops-157306},
  doi =		{10.4230/LIPIcs.CSL.2022.10},
  annote =	{Keywords: Games on graphs, subgame-perfect equilibria, parity objectives}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.8
Subgame-Perfect Equilibria in Mean-Payoff Games

Authors: Léonard Brice, Jean-François Raskin, and Marie van den Bogaard

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
In this paper, we provide an effective characterization of all the subgame-perfect equilibria in infinite duration games played on finite graphs with mean-payoff objectives. To this end, we introduce the notion of requirement, and the notion of negotiation function. We establish that the plays that are supported by SPEs are exactly those that are consistent with the least fixed point of the negotiation function. Finally, we show that the negotiation function is piecewise linear, and can be analyzed using the linear algebraic tool box. As a corollary, we prove the decidability of the SPE constrained existence problem, whose status was left open in the literature.
Cite as

Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. Subgame-Perfect Equilibria in Mean-Payoff Games. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{brice_et_al:LIPIcs.CONCUR.2021.8,
  author =	{Brice, L\'{e}onard and Raskin, Jean-Fran\c{c}ois and van den Bogaard, Marie},
  title =	{{Subgame-Perfect Equilibria in Mean-Payoff Games}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{8:1--8:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.8},
  URN =		{urn:nbn:de:0030-drops-143854},
  doi =		{10.4230/LIPIcs.CONCUR.2021.8},
  annote =	{Keywords: Games on graphs, subgame-perfect equilibria, mean-payoff objectives.}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.9
Fragility and Robustness in Mean-Payoff Adversarial Stackelberg Games

Authors: Mrudula Balachander, Shibashis Guha, and Jean-François Raskin

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
Two-player mean-payoff Stackelberg games are nonzero-sum infinite duration games played on a bi-weighted graph by Leader (Player 0) and Follower (Player 1). Such games are played sequentially: first, Leader announces her strategy, second, Follower chooses his best-response. If we cannot impose which best-response is chosen by Follower, we say that Follower, though strategic, is adversarial towards Leader. The maximal value that Leader can get in this nonzero-sum game is called the adversarial Stackelberg value (ASV) of the game. We study the robustness of strategies for Leader in these games against two types of deviations: (i) Modeling imprecision - the weights on the edges of the game arena may not be exactly correct, they may be delta-away from the right one. (ii) Sub-optimal response - Follower may play epsilon-optimal best-responses instead of perfect best-responses. First, we show that if the game is zero-sum then robustness is guaranteed while in the nonzero-sum case, optimal strategies for ASV are fragile. Second, we provide a solution concept to obtain strategies for Leader that are robust to both modeling imprecision, and as well as to the epsilon-optimal responses of Follower, and study several properties and algorithmic problems related to this solution concept.
Cite as

Mrudula Balachander, Shibashis Guha, and Jean-François Raskin. Fragility and Robustness in Mean-Payoff Adversarial Stackelberg Games. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{balachander_et_al:LIPIcs.CONCUR.2021.9,
  author =	{Balachander, Mrudula and Guha, Shibashis and Raskin, Jean-Fran\c{c}ois},
  title =	{{Fragility and Robustness in Mean-Payoff Adversarial Stackelberg Games}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{9:1--9:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.9},
  URN =		{urn:nbn:de:0030-drops-143863},
  doi =		{10.4230/LIPIcs.CONCUR.2021.9},
  annote =	{Keywords: mean-payoff, Stackelberg games, synthesis}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.27
Stackelberg-Pareto Synthesis

Authors: Véronique Bruyère, Jean-François Raskin, and Clément Tamines

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
In this paper, we study the framework of two-player Stackelberg games played on graphs in which Player 0 announces a strategy and Player 1 responds rationally with a strategy that is an optimal response. While it is usually assumed that Player 1 has a single objective, we consider here the new setting where he has several. In this context, after responding with his strategy, Player 1 gets a payoff in the form of a vector of Booleans corresponding to his satisfied objectives. Rationality of Player 1 is encoded by the fact that his response must produce a Pareto-optimal payoff given the strategy of Player 0. We study the Stackelberg-Pareto Synthesis problem which asks whether Player 0 can announce a strategy which satisfies his objective, whatever the rational response of Player 1. For games in which objectives are either all parity or all reachability objectives, we show that this problem is fixed-parameter tractable and NEXPTIME-complete. This problem is already NP-complete in the simple case of reachability objectives and graphs that are trees.
Cite as

Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Stackelberg-Pareto Synthesis. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2021.27,
  author =	{Bruy\`{e}re, V\'{e}ronique and Raskin, Jean-Fran\c{c}ois and Tamines, Cl\'{e}ment},
  title =	{{Stackelberg-Pareto Synthesis}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.27},
  URN =		{urn:nbn:de:0030-drops-144040},
  doi =		{10.4230/LIPIcs.CONCUR.2021.27},
  annote =	{Keywords: Stackelberg non-zero sum games played on graphs, synthesis, parity objectives}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.17
Weighted Transducers for Robustness Verification

Authors: Emmanuel Filiot, Nicolas Mazzocchi, Jean-François Raskin, Sriram Sankaranarayanan, and Ashutosh Trivedi

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
Automata theory provides us with fundamental notions such as languages, membership, emptiness and inclusion that in turn allow us to specify and verify properties of reactive systems in a useful manner. However, these notions all yield "yes"/"no" answers that sometimes fall short of being satisfactory answers when the models being analyzed are imperfect, and the observations made are prone to errors. To address this issue, a common engineering approach is not just to verify that a system satisfies a property, but whether it does so robustly. We present notions of robustness that place a metric on words, thus providing a natural notion of distance between words. Such a metric naturally leads to a topological neighborhood of words and languages, leading to quantitative and robust versions of the membership, emptiness and inclusion problems. More generally, we consider weighted transducers to model the cost of errors. Such a transducer models neighborhoods of words by providing the cost of rewriting a word into another. The main contribution of this work is to study robustness verification problems in the context of weighted transducers. We provide algorithms for solving the robust and quantitative versions of the membership and inclusion problems while providing useful motivating case studies including approximate pattern matching problems to detect clinically relevant events in a large type-1 diabetes dataset.
Cite as

Emmanuel Filiot, Nicolas Mazzocchi, Jean-François Raskin, Sriram Sankaranarayanan, and Ashutosh Trivedi. Weighted Transducers for Robustness Verification. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 17:1-17:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.CONCUR.2020.17,
  author =	{Filiot, Emmanuel and Mazzocchi, Nicolas and Raskin, Jean-Fran\c{c}ois and Sankaranarayanan, Sriram and Trivedi, Ashutosh},
  title =	{{Weighted Transducers for Robustness Verification}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{17:1--17:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.17},
  URN =		{urn:nbn:de:0030-drops-128290},
  doi =		{10.4230/LIPIcs.CONCUR.2020.17},
  annote =	{Keywords: Weighted transducers, Quantitative verification, Fault-tolerance}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.40
Monte Carlo Tree Search Guided by Symbolic Advice for MDPs

Authors: Damien Busatto-Gaston, Debraj Chakraborty, and Jean-Francois Raskin

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
In this paper, we consider the online computation of a strategy that aims at optimizing the expected average reward in a Markov decision process. The strategy is computed with a receding horizon and using Monte Carlo tree search (MCTS). We augment the MCTS algorithm with the notion of symbolic advice, and show that its classical theoretical guarantees are maintained. Symbolic advice are used to bias the selection and simulation strategies of MCTS. We describe how to use QBF and SAT solvers to implement symbolic advice in an efficient way. We illustrate our new algorithm using the popular game Pac-Man and show that the performances of our algorithm exceed those of plain MCTS as well as the performances of human players.
Cite as

Damien Busatto-Gaston, Debraj Chakraborty, and Jean-Francois Raskin. Monte Carlo Tree Search Guided by Symbolic Advice for MDPs. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 40:1-40:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{busattogaston_et_al:LIPIcs.CONCUR.2020.40,
  author =	{Busatto-Gaston, Damien and Chakraborty, Debraj and Raskin, Jean-Francois},
  title =	{{Monte Carlo Tree Search Guided by Symbolic Advice for MDPs}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{40:1--40:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.40},
  URN =		{urn:nbn:de:0030-drops-128523},
  doi =		{10.4230/LIPIcs.CONCUR.2020.40},
  annote =	{Keywords: Markov decision process, Monte Carlo tree search, symbolic advice, simulation}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.127
The Adversarial Stackelberg Value in Quantitative Games

Authors: Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
In this paper, we study the notion of adversarial Stackelberg value for two-player non-zero sum games played on bi-weighted graphs with the mean-payoff and the discounted sum functions. The adversarial Stackelberg value of Player 0 is the largest value that Player 0 can obtain when announcing her strategy to Player 1 which in turn responds with any of his best response. For the mean-payoff function, we show that the adversarial Stackelberg value is not always achievable but ε-optimal strategies exist. We show how to compute this value and prove that the associated threshold problem is in NP. For the discounted sum payoff function, we draw a link with the target discounted sum problem which explains why the problem is difficult to solve for this payoff function. We also provide solutions to related gap problems.
Cite as

Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin. The Adversarial Stackelberg Value in Quantitative Games. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 127:1-127:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.ICALP.2020.127,
  author =	{Filiot, Emmanuel and Gentilini, Raffaella and Raskin, Jean-Fran\c{c}ois},
  title =	{{The Adversarial Stackelberg Value in Quantitative Games}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{127:1--127:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.127},
  URN =		{urn:nbn:de:0030-drops-125348},
  doi =		{10.4230/LIPIcs.ICALP.2020.127},
  annote =	{Keywords: Non-zero sum games, reactive synthesis, adversarial Stackelberg}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2019.32
Expected Window Mean-Payoff

Authors: Benjamin Bordais, Shibashis Guha, and Jean-François Raskin

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)

Abstract
We study the expected value of the window mean-payoff measure in Markov decision processes (MDPs) and Markov chains (MCs). The window mean-payoff measure strengthens the classical mean-payoff measure by measuring the mean-payoff over a window of bounded length that slides along an infinite path. This measure ensures better stability properties than the classical mean-payoff. Window mean-payoff has been introduced previously for two-player zero-sum games. As in the case of games, we study several variants of this definition: the measure can be defined to be prefix-independent or not, and for a fixed window length or for a window length that is left parametric. For fixed window length, we provide polynomial time algorithms for the prefix-independent version for both MDPs and MCs. When the length is left parametric, the problem of computing the expected value on MDPs is as hard as computing the mean-payoff value in two-player zero-sum games, a problem for which it is not known if it can be solved in polynomial time. For the prefix-dependent version, surprisingly, the expected window mean-payoff value cannot be computed in polynomial time unless P=PSPACE. For the parametric case and the prefix-dependent case, we manage to obtain algorithms with better complexities for MCs.
Cite as

Benjamin Bordais, Shibashis Guha, and Jean-François Raskin. Expected Window Mean-Payoff. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 32:1-32:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bordais_et_al:LIPIcs.FSTTCS.2019.32,
  author =	{Bordais, Benjamin and Guha, Shibashis and Raskin, Jean-Fran\c{c}ois},
  title =	{{Expected Window Mean-Payoff}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{32:1--32:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.32},
  URN =		{urn:nbn:de:0030-drops-115940},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.32},
  annote =	{Keywords: mean-payoff, Markov decision processes, synthesis}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.13
The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games

Authors: Thomas Brihaye, Véronique Bruyère, Aline Goeminne, Jean-François Raskin, and Marie van den Bogaard

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
We study multiplayer quantitative reachability games played on a finite directed graph, where the objective of each player is to reach his target set of vertices as quickly as possible. Instead of the well-known notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium (SPE), a refinement of NE well-suited in the framework of games played on graphs. It is known that there always exists an SPE in quantitative reachability games and that the constrained existence problem is decidable. We here prove that this problem is PSPACE-complete. To obtain this result, we propose a new algorithm that iteratively builds a set of constraints characterizing the set of SPE outcomes in quantitative reachability games. This set of constraints is obtained by iterating an operator that reinforces the constraints up to obtaining a fixpoint. With this fixpoint, the set of SPE outcomes can be represented by a finite graph of size at most exponential. A careful inspection of the computation allows us to establish PSPACE membership.
Cite as

Thomas Brihaye, Véronique Bruyère, Aline Goeminne, Jean-François Raskin, and Marie van den Bogaard. The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.CONCUR.2019.13,
  author =	{Brihaye, Thomas and Bruy\`{e}re, V\'{e}ronique and Goeminne, Aline and Raskin, Jean-Fran\c{c}ois and van den Bogaard, Marie},
  title =	{{The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{13:1--13:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.13},
  URN =		{urn:nbn:de:0030-drops-109153},
  doi =		{10.4230/LIPIcs.CONCUR.2019.13},
  annote =	{Keywords: multiplayer non-zero-sum games played on graphs, quantitative reachability objectives, subgame perfect equilibria, constrained existence problem}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.21
Energy Mean-Payoff Games

Authors: Véronique Bruyère, Quentin Hautem, Mickael Randour, and Jean-François Raskin

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
In this paper, we study one-player and two-player energy mean-payoff games. Energy mean-payoff games are games of infinite duration played on a finite graph with edges labeled by 2-dimensional weight vectors. The objective of the first player (the protagonist) is to satisfy an energy objective on the first dimension and a mean-payoff objective on the second dimension. We show that optimal strategies for the first player may require infinite memory while optimal strategies for the second player (the antagonist) do not require memory. In the one-player case (where only the first player has choices), the problem of deciding who is the winner can be solved in polynomial time while for the two-player case we show co-NP membership and we give effective constructions for the infinite-memory optimal strategies of the protagonist.
Cite as

Véronique Bruyère, Quentin Hautem, Mickael Randour, and Jean-François Raskin. Energy Mean-Payoff Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2019.21,
  author =	{Bruy\`{e}re, V\'{e}ronique and Hautem, Quentin and Randour, Mickael and Raskin, Jean-Fran\c{c}ois},
  title =	{{Energy Mean-Payoff Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{21:1--21:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.21},
  URN =		{urn:nbn:de:0030-drops-109239},
  doi =		{10.4230/LIPIcs.CONCUR.2019.21},
  annote =	{Keywords: two-player zero-sum games played on graphs, energy and mean-payoff objectives, complexity study and construction of optimal strategies}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.36
Safe and Optimal Scheduling for Hard and Soft Tasks

Authors: Gilles Geeraerts, Shibashis Guha, and Jean-François Raskin

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
We consider a stochastic scheduling problem with both hard and soft tasks on a single machine. Each task is described by a discrete probability distribution over possible execution times, and possible inter-arrival times of the job, and a fixed deadline. Soft tasks also carry a penalty cost to be paid when they miss a deadline. We ask to compute an online and non-clairvoyant scheduler (i.e. one that must take decisions without knowing the future evolution of the system) that is safe and efficient. Safety imposes that deadline of hard tasks are never violated while efficient means that we want to minimise the mean cost of missing deadlines by soft tasks. First, we show that the dynamics of such a system can be modelled as a finite Markov Decision Process (MDP). Second, we show that our scheduling problem is PP-hard and in EXPTime. Third, we report on a prototype tool that solves our scheduling problem by relying on the Storm tool to analyse the corresponding MDP. We show how antichain techniques can be used as a potential heuristic.
Cite as

Gilles Geeraerts, Shibashis Guha, and Jean-François Raskin. Safe and Optimal Scheduling for Hard and Soft Tasks. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 36:1-36:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{geeraerts_et_al:LIPIcs.FSTTCS.2018.36,
  author =	{Geeraerts, Gilles and Guha, Shibashis and Raskin, Jean-Fran\c{c}ois},
  title =	{{Safe and Optimal Scheduling for Hard and Soft Tasks}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{36:1--36:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.36},
  URN =		{urn:nbn:de:0030-drops-99352},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.36},
  annote =	{Keywords: Non-clairvoyant scheduling, hard and soft tasks, automatic synthesis, Markov decision processes}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.8
Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints

Authors: Jan Kretínský, Guillermo A. Pérez, and Jean-François Raskin

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
We formalize the problem of maximizing the mean-payoff value with high probability while satisfying a parity objective in a Markov decision process (MDP) with unknown probabilistic transition function and unknown reward function. Assuming the support of the unknown transition function and a lower bound on the minimal transition probability are known in advance, we show that in MDPs consisting of a single end component, two combinations of guarantees on the parity and mean-payoff objectives can be achieved depending on how much memory one is willing to use. (i) For all epsilon and gamma we can construct an online-learning finite-memory strategy that almost-surely satisfies the parity objective and which achieves an epsilon-optimal mean payoff with probability at least 1 - gamma. (ii) Alternatively, for all epsilon and gamma there exists an online-learning infinite-memory strategy that satisfies the parity objective surely and which achieves an epsilon-optimal mean payoff with probability at least 1 - gamma. We extend the above results to MDPs consisting of more than one end component in a natural way. Finally, we show that the aforementioned guarantees are tight, i.e. there are MDPs for which stronger combinations of the guarantees cannot be ensured.
Cite as

Jan Kretínský, Guillermo A. Pérez, and Jean-François Raskin. Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kretinsky_et_al:LIPIcs.CONCUR.2018.8,
  author =	{Kret{\'\i}nsk\'{y}, Jan and P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  title =	{{Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.8},
  URN =		{urn:nbn:de:0030-drops-95468},
  doi =		{10.4230/LIPIcs.CONCUR.2018.8},
  annote =	{Keywords: Markov decision processes, Reinforcement learning, Beyond worst case}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.29
Parameterized complexity of games with monotonically ordered omega-regular objectives

Authors: Véronique Bruyère, Quentin Hautem, and Jean-François Raskin

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
In recent years, two-player zero-sum games with multiple objectives have received a lot of interest as a model for the synthesis of complex reactive systems. In this framework, Player 1 wins if he can ensure that all objectives are satisfied against any behavior of Player 2. When this is not possible to satisfy all the objectives at once, an alternative is to use some preorder on the objectives according to which subset of objectives Player 1 wants to satisfy. For example, it is often natural to provide more significance to one objective over another, a situation that can be modelled with lexicographically ordered objectives for instance. Inspired by recent work on concurrent games with multiple omega-regular objectives by Bouyer et al., we investigate in detail turned-based games with monotonically ordered and omega-regular objectives. We study the threshold problem which asks whether player 1 can ensure a payoff greater than or equal to a given threshold w.r.t. a given monotonic preorder. As the number of objectives is usually much smaller than the size of the game graph, we provide a parametric complexity analysis and we show that our threshold problem is in FPT for all monotonic preorders and all classical types of omega-regular objectives. We also provide polynomial time algorithms for Büchi, coBüchi and explicit Muller objectives for a large subclass of monotonic preorders that includes among others the lexicographic preorder. In the particular case of lexicographic preorder, we also study the complexity of computing the values and the memory requirements of optimal strategies.
Cite as

Véronique Bruyère, Quentin Hautem, and Jean-François Raskin. Parameterized complexity of games with monotonically ordered omega-regular objectives. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2018.29,
  author =	{Bruy\`{e}re, V\'{e}ronique and Hautem, Quentin and Raskin, Jean-Fran\c{c}ois},
  title =	{{Parameterized complexity of games with monotonically ordered omega-regular objectives}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{29:1--29:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.29},
  URN =		{urn:nbn:de:0030-drops-95673},
  doi =		{10.4230/LIPIcs.CONCUR.2018.29},
  annote =	{Keywords: two-player zero-sum games played on graphs, omega-regular objectives, ordered objectives, parameterized complexity}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.10
Beyond Admissibility: Dominance Between Chains of Strategies

Authors: Nicolas Basset, Ismaël Jecker, Arno Pauly, Jean-François Raskin, and Marie Van den Bogaard

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Admissible strategies, i.e. those that are not dominated by any other strategy, are a typical rationality notion in game theory. In many classes of games this is justified by results showing that any strategy is admissible or dominated by an admissible strategy. However, in games played on finite graphs with quantitative objectives (as used for reactive synthesis), this is not the case. We consider increasing chains of strategies instead to recover a satisfactory rationality notion based on dominance in such games. We start with some order-theoretic considerations establishing sufficient criteria for this to work. We then turn our attention to generalised safety/reachability games as a particular application. We propose the notion of maximal uniform chain as the desired dominance-based rationality concept in these games. Decidability of some fundamental questions about uniform chains is established.
Cite as

Nicolas Basset, Ismaël Jecker, Arno Pauly, Jean-François Raskin, and Marie Van den Bogaard. Beyond Admissibility: Dominance Between Chains of Strategies. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{basset_et_al:LIPIcs.CSL.2018.10,
  author =	{Basset, Nicolas and Jecker, Isma\"{e}l and Pauly, Arno and Raskin, Jean-Fran\c{c}ois and Van den Bogaard, Marie},
  title =	{{Beyond Admissibility: Dominance Between Chains of Strategies}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{10:1--10:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.10},
  URN =		{urn:nbn:de:0030-drops-96774},
  doi =		{10.4230/LIPIcs.CSL.2018.10},
  annote =	{Keywords: dominated strategies, admissible strategies, games played on finite graphs, reactive synthesis, reachability games, safety games, cofinal, order theory}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.MFCS.2017
LIPIcs, Volume 83, MFCS'17, Complete Volume

Authors: Kim G. Larsen, Hans L. Bodlaender, and Jean-Francois Raskin

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
LIPIcs, Volume 83, MFCS'17, Complete Volume
Cite as

42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Proceedings{larsen_et_al:LIPIcs.MFCS.2017,
  title =	{{LIPIcs, Volume 83, MFCS'17, Complete Volume}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017},
  URN =		{urn:nbn:de:0030-drops-82073},
  doi =		{10.4230/LIPIcs.MFCS.2017},
  annote =	{Keywords: Theory of Computation}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.MFCS.2017.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Kim G. Larsen, Hans L. Bodlaender, and Jean-Francois Raskin

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{larsen_et_al:LIPIcs.MFCS.2017.0,
  author =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{0:i--0:xvi},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.0},
  URN =		{urn:nbn:de:0030-drops-80564},
  doi =		{10.4230/LIPIcs.MFCS.2017.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2017.2
Admissibility in Games with Imperfect Information (Invited Talk)

Authors: Romain Brenguier, Arno Pauly, Jean-François Raskin, and Ocan Sankur

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
In this invited paper, we study the concept of admissible strategies for two player win/lose infinite sequential games with imperfect information. We show that in stark contrast with the perfect information variant, admissible strategies are only guaranteed to exist when players have objectives that are closed sets. As a consequence, we also study decision problems related to the existence of admissible strategies for regular games as well as finite duration games.
Cite as

Romain Brenguier, Arno Pauly, Jean-François Raskin, and Ocan Sankur. Admissibility in Games with Imperfect Information (Invited Talk). In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{brenguier_et_al:LIPIcs.CONCUR.2017.2,
  author =	{Brenguier, Romain and Pauly, Arno and Raskin, Jean-Fran\c{c}ois and Sankur, Ocan},
  title =	{{Admissibility in Games with Imperfect Information}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{2:1--2:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.2},
  URN =		{urn:nbn:de:0030-drops-78066},
  doi =		{10.4230/LIPIcs.CONCUR.2017.2},
  annote =	{Keywords: Admissibility, non-zero sum games, reactive synthesis, imperfect infor- mation}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.121
Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes

Authors: Raphaël Berthon, Mickael Randour, and Jean-François Raskin

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
The beyond worst-case synthesis problem was introduced recently by Bruyère et al. [BFRR14]: it aims at building system controllers that provide strict worst-case performance guarantees against an antagonistic environment while ensuring higher expected performance against a stochastic model of the environment. Our work extends the framework of [Bruyère/Filiot/Randour/Raskin, STACS 2014] and follow-up papers, which focused on quantitative objectives, by addressing the case of omega-regular conditions encoded as parity objectives, a natural way to represent functional requirements of systems. We build strategies that satisfy a main parity objective on all plays, while ensuring a secondary one with sufficient probability. This setting raises new challenges in comparison to quantitative objectives, as one cannot easily mix different strategies without endangering the functional properties of the system. We establish that, for all variants of this problem, deciding the existence of a strategy lies in NP and in coNP, the same complexity class as classical parity games. Hence, our framework provides additional modeling power while staying in the same complexity class.
Cite as

Raphaël Berthon, Mickael Randour, and Jean-François Raskin. Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 121:1-121:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{berthon_et_al:LIPIcs.ICALP.2017.121,
  author =	{Berthon, Rapha\"{e}l and Randour, Mickael and Raskin, Jean-Fran\c{c}ois},
  title =	{{Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{121:1--121:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.121},
  URN =		{urn:nbn:de:0030-drops-74360},
  doi =		{10.4230/LIPIcs.ICALP.2017.121},
  annote =	{Keywords: Markov decision processes, parity objectives, beyond worst-case synthesis}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.123
Admissiblity in Concurrent Games

Authors: Nicolas Basset, Gilles Geeraerts, Jean-François Raskin, and Ocan Sankur

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
In this paper, we study the notion of admissibility for randomised strategies in concurrent games. Intuitively, an admissible strategy is one where the player plays 'as well as possible', because there is no other strategy that dominates it, i.e., that wins (almost surely) against a superset of adversarial strategies. We prove that admissible strategies always exist in concurrent games, and we characterise them precisely. Then, when the objectives of the players are omega-regular, we show how to perform assume-admissible synthesis, i.e., how to compute admissible strategies that win (almost surely) under the hypothesis that the other players play admissible strategies only.
Cite as

Nicolas Basset, Gilles Geeraerts, Jean-François Raskin, and Ocan Sankur. Admissiblity in Concurrent Games. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 123:1-123:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{basset_et_al:LIPIcs.ICALP.2017.123,
  author =	{Basset, Nicolas and Geeraerts, Gilles and Raskin, Jean-Fran\c{c}ois and Sankur, Ocan},
  title =	{{Admissiblity in Concurrent Games}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{123:1--123:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.123},
  URN =		{urn:nbn:de:0030-drops-74765},
  doi =		{10.4230/LIPIcs.ICALP.2017.123},
  annote =	{Keywords: Multi-player games, admissibility, concurrent games, randomized strategies}
}
Document
DOI: 10.4230/LIPIcs.STACS.2017.50
Minkowski Games

Authors: Stéphane Le Roux, Arno Pauly, and Jean-François Raskin

Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)

Abstract
We introduce and study Minkowski games. In these games, two players take turns to choose positions in R^d based on some rules. Variants include boundedness games, where one player wants to keep the positions bounded (while the other wants to escape to infinity), and safety games, where one player wants to stay within a given set (while the other wants to leave it). We provide some general characterizations of which player can win such games, and explore the computational complexity of the associated decision problems. A natural representation of boundedness games yields coNP-completeness, whereas the safety games are undecidable.
Cite as

Stéphane Le Roux, Arno Pauly, and Jean-François Raskin. Minkowski Games. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 50:1-50:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{leroux_et_al:LIPIcs.STACS.2017.50,
  author =	{Le Roux, St\'{e}phane and Pauly, Arno and Raskin, Jean-Fran\c{c}ois},
  title =	{{Minkowski Games}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{50:1--50:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Vollmer, Heribert and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.50},
  URN =		{urn:nbn:de:0030-drops-69849},
  doi =		{10.4230/LIPIcs.STACS.2017.50},
  annote =	{Keywords: Control in R^d, determinacy, polytopic/arbitrary, coNP-complete, undecidable}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.42
Admissibility in Quantitative Graph Games

Authors: Romain Brenguier, Guillermo A. Pérez, Jean-Francois Raskin, and Ocan Sankur

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
Admissibility has been studied for games of infinite duration with Boolean objectives. We extend here this study to games of infinite duration with quantitative objectives. First, we show that, under the assumption that optimal worst-case and cooperative strategies exist, admissible strategies are guaranteed to exist. Second, we give a characterization of admissible strategies using the notion of adversarial and cooperative values of a history, and we characterize the set of outcomes that are compatible with admissible strategies. Finally, we show how these characterizations can be used to design algorithms to decide relevant verification and synthesis problems.
Cite as

Romain Brenguier, Guillermo A. Pérez, Jean-Francois Raskin, and Ocan Sankur. Admissibility in Quantitative Graph Games. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 42:1-42:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{brenguier_et_al:LIPIcs.FSTTCS.2016.42,
  author =	{Brenguier, Romain and P\'{e}rez, Guillermo A. and Raskin, Jean-Francois and Sankur, Ocan},
  title =	{{Admissibility in Quantitative Graph Games}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{42:1--42:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.42},
  URN =		{urn:nbn:de:0030-drops-68772},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.42},
  annote =	{Keywords: Quantitative games, Verification, Reactive synthesis, Admissibility}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.30
Minimizing Regret in Discounted-Sum Games

Authors: Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
In this paper, we study the problem of minimizing regret in discounted-sum games played on weighted game graphs. We give algorithms for the general problem of computing the minimal regret of the controller (Eve) as well as several variants depending on which strategies the environment (Adam) is permitted to use. We also consider the problem of synthesizing regret-free strategies for Eve in each of these scenarios.
Cite as

Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Minimizing Regret in Discounted-Sum Games. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{hunter_et_al:LIPIcs.CSL.2016.30,
  author =	{Hunter, Paul and P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  title =	{{Minimizing Regret in Discounted-Sum Games}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{30:1--30:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.30},
  URN =		{urn:nbn:de:0030-drops-65704},
  doi =		{10.4230/LIPIcs.CSL.2016.30},
  annote =	{Keywords: Quantitative games, Regret, Verification, Synthesis, Game theory}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.11
On the Complexity of Heterogeneous Multidimensional Games

Authors: Veronique Bruyere, Quentin Hautem, and Jean-Francois Raskin

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
We study two-player zero-sum turn-based games played on multidimensional weighted graphs with heterogeneous quantitative objectives. Our objectives are defined starting from the measures Inf, Sup, LimInf, and LimSup of the weights seen along the play, as well as on the window mean-payoff (WMP) measure recently introduced in [Krishnendu,Doyen,Randour,Raskin, Inf. Comput., 2015]. Whereas multidimensional games with Boolean combinations of classical mean-payoff objectives are undecidable [Velner, FOSSACS, 2015], we show that CNF/DNF Boolean combinations for heterogeneous measures taken among {WMP, Inf, Sup, LimInf, LimSup} lead to EXPTIME-completeness with exponential memory strategies for both players. We also identify several interesting fragments with better complexities and memory requirements, and show that some of them are solvable in PTIME.
Cite as

Veronique Bruyere, Quentin Hautem, and Jean-Francois Raskin. On the Complexity of Heterogeneous Multidimensional Games. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 11:1-11:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.CONCUR.2016.11,
  author =	{Bruyere, Veronique and Hautem, Quentin and Raskin, Jean-Francois},
  title =	{{On the Complexity of Heterogeneous Multidimensional Games}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{11:1--11:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.11},
  URN =		{urn:nbn:de:0030-drops-61618},
  doi =		{10.4230/LIPIcs.CONCUR.2016.11},
  annote =	{Keywords: wo-player zero-sum games played on graphs, quantitative objectives, multidimensional heterogeneous objectives}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.121
The Complexity of Rational Synthesis

Authors: Rodica Condurache, Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
We study the computational complexity of the cooperative and non-cooperative rational synthesis problems, as introduced by Kupferman, Vardi and co-authors. We provide tight results for most of the classical omega-regular objectives, and show how to solve those problems optimally.
Cite as

Rodica Condurache, Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin. The Complexity of Rational Synthesis. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 121:1-121:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{condurache_et_al:LIPIcs.ICALP.2016.121,
  author =	{Condurache, Rodica and Filiot, Emmanuel and Gentilini, Raffaella and Raskin, Jean-Fran\c{c}ois},
  title =	{{The Complexity of Rational Synthesis}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{121:1--121:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.121},
  URN =		{urn:nbn:de:0030-drops-62565},
  doi =		{10.4230/LIPIcs.ICALP.2016.121},
  annote =	{Keywords: Non-zero sum games, reactive synthesis, omega-regular objectives}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.504
Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability

Authors: Thomas Brihaye, Véronique Bruyère, Noémie Meunier, and Jean-Francois Raskin

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
We study n-player turn-based games played on a finite directed graph. For each play, the players have to pay a cost that they want to minimize. Instead of the well-known notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium (SPE), a refinement of NE well-suited in the framework of games played on graphs. We also study natural variants of SPE, named weak (resp. very weak) SPE, where players who deviate cannot use the full class of strategies but only a subclass with a finite number of (resp. a unique) deviation step(s). Our results are threefold. Firstly, we characterize in the form of a Folk theorem the set of all plays that are the outcome of a weak SPE. Secondly, for the class of quantitative reachability games, we prove the existence of a finite-memory SPE and provide an algorithm for computing it (only existence was known with no information regarding the memory). Moreover, we show that the existence of a constrained SPE, i.e. an SPE such that each player pays a cost less than a given constant, can be decided. The proofs rely on our Folk theorem for weak SPEs (which coincide with SPEs in the case of quantitative reachability games) and on the decidability of MSO logic on infinite words. Finally with similar techniques, we provide a second general class of games for which the existence of a (constrained) weak SPE is decidable.
Cite as

Thomas Brihaye, Véronique Bruyère, Noémie Meunier, and Jean-Francois Raskin. Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 504-518, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.CSL.2015.504,
  author =	{Brihaye, Thomas and Bruy\`{e}re, V\'{e}ronique and Meunier, No\'{e}mie and Raskin, Jean-Francois},
  title =	{{Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{504--518},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.504},
  URN =		{urn:nbn:de:0030-drops-54345},
  doi =		{10.4230/LIPIcs.CSL.2015.504},
  annote =	{Keywords: multi-player games on graphs, quantitative objectives, Nash equilibrium, subgame perfect equilibrium, quantitative reachability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.100
Assume-Admissible Synthesis

Authors: Romain Brenguier, Jean-François Raskin, and Ocan Sankur

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
In this paper, we introduce a novel rule for synthesis of reactive systems, applicable to systems made of n components which have each their own objectives. It is based on the notion of admissible strategies. We compare our novel rule with previous rules defined in the literature, and we show that contrary to the previous proposals, our rule define sets of solutions which are rectangular. This property leads to solutions which are robust and resilient. We provide algorithms with optimal complexity and also an abstraction framework.
Cite as

Romain Brenguier, Jean-François Raskin, and Ocan Sankur. Assume-Admissible Synthesis. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 100-113, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{brenguier_et_al:LIPIcs.CONCUR.2015.100,
  author =	{Brenguier, Romain and Raskin, Jean-Fran\c{c}ois and Sankur, Ocan},
  title =	{{Assume-Admissible Synthesis}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{100--113},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.100},
  URN =		{urn:nbn:de:0030-drops-53711},
  doi =		{10.4230/LIPIcs.CONCUR.2015.100},
  annote =	{Keywords: Multi-player games, controller synthesis, admissibility}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.114
Reactive Synthesis Without Regret

Authors: Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Two-player zero-sum games of infinite duration and their quantitative versions are used in verification to model the interaction between a controller (Eve) and its environment (Adam). The question usually addressed is that of the existence (and computability) of a strategy for Eve that can maximize her payoff against any strategy of Adam. In this work, we are interested in strategies of Eve that minimize her regret, i.e. strategies that minimize the difference between her actual payoff and the payoff she could have achieved if she had known the strategy of Adam in advance. We give algorithms to compute the strategies of Eve that ensure minimal regret against an adversary whose choice of strategy is (i) unrestricted, (ii) limited to positional strategies, or (iii) limited to word strategies, and show that the two last cases have natural modelling applications. We also show that our notion of regret minimization in which Adam is limited to word strategies generalizes the notion of good for games introduced by Henzinger and Piterman, and is related to the notion of determinization by pruning due to Aminof, Kupferman and Lampert.
Cite as

Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Reactive Synthesis Without Regret. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 114-127, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{hunter_et_al:LIPIcs.CONCUR.2015.114,
  author =	{Hunter, Paul and P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  title =	{{Reactive Synthesis Without Regret}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{114--127},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.114},
  URN =		{urn:nbn:de:0030-drops-53675},
  doi =		{10.4230/LIPIcs.CONCUR.2015.114},
  annote =	{Keywords: Quantitative games, regret, verification, synthesis, game theory}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.133
Finite-Valued Weighted Automata

Authors: Emmanuel Filiot, Raffaella Gentilini, and Jean-Francois Raskin

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
Any weighted automaton (WA) defines a relation from finite words to values: given an input word, its set of values is obtained as the set of values computed by each accepting run on that word. A WA is k-valued if the relation it defines has degree at most k, i.e., every set of values associated with an input word has cardinality at most k. We investigate the class of quantitative languages defined by k-valued automata, for all parameters k. We consider several measures to associate values with runs: sum, discounted-sum, and more generally values in groups. We define a general procedure which decides, given a bound k and a WA over a group, whether this automaton is k-valued. We also show that any k-valued WA over a group, under some general conditions, can be decomposed as a union of k unambiguous WA. While inclusion and equivalence are undecidable problems for arbitrary sum-automata, we show, based on this decomposition, that they are decidable for k-valued sum-automata, and k-valued discounted sum-automata over inverted integer discount factors. We finally show that the quantitative Church problem is undecidable for k-valued sum-automata, even given as finite unions of deterministic sum-automata.
Cite as

Emmanuel Filiot, Raffaella Gentilini, and Jean-Francois Raskin. Finite-Valued Weighted Automata. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 133-145, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.FSTTCS.2014.133,
  author =	{Filiot, Emmanuel and Gentilini, Raffaella and Raskin, Jean-Francois},
  title =	{{Finite-Valued Weighted Automata}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{133--145},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.133},
  URN =		{urn:nbn:de:0030-drops-48388},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.133},
  annote =	{Keywords: Nested word, Transducer, Streaming}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.365
Quantitative Games with Interval Objectives

Authors: Paul Hunter and Jean-Francois Raskin

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
Traditionally quantitative games such as mean-payoff games and discount sum games have two players - one trying to maximize the payoff, the other trying to minimize it. The associated decision problem, "Can Eve (the maximizer) achieve, for example, a positive payoff?" can be thought of as one player trying to attain a payoff in the interval (0,infinity). In this paper we consider the more general problem of determining if a player can attain a payoff in a finite union of arbitrary intervals for various payoff functions (liminf/limsup, mean-payoff, discount sum, total sum). In particular this includes the interesting exact-value problem, "Can Eve achieve a payoff of exactly (e.g.) 0?"
Cite as

Paul Hunter and Jean-Francois Raskin. Quantitative Games with Interval Objectives. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 365-377, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{hunter_et_al:LIPIcs.FSTTCS.2014.365,
  author =	{Hunter, Paul and Raskin, Jean-Francois},
  title =	{{Quantitative Games with Interval Objectives}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{365--377},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.365},
  URN =		{urn:nbn:de:0030-drops-48569},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.365},
  annote =	{Keywords: Quantitative games, Mean-payoff games, Discount sum games}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.531
Multiple-Environment Markov Decision Processes

Authors: Jean-Francois Raskin and Ocan Sankur

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We introduce Multi-Environment Markov Decision Processes (MEMDPs) which are MDPs with a set of probabilistic transition functions. The goal in an MEMDP is to synthesize a single controller strategy with guaranteed performances against all environments even though the environment is unknown a priori. While MEMDPs can be seen as a special class of partially observable MDPs, we show that several verification problems that are undecidable for partially observable MDPs, are decidable for MEMDPs and sometimes have even efficient solutions.
Cite as

Jean-Francois Raskin and Ocan Sankur. Multiple-Environment Markov Decision Processes. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 531-543, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{raskin_et_al:LIPIcs.FSTTCS.2014.531,
  author =	{Raskin, Jean-Francois and Sankur, Ocan},
  title =	{{Multiple-Environment Markov Decision Processes}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{531--543},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.531},
  URN =		{urn:nbn:de:0030-drops-48692},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.531},
  annote =	{Keywords: Markov decision processes, probabilistic systems, multiple objectives}
}
Document
DOI: 10.4230/LIPIcs.STACS.2014.199
Meet Your Expectations With Guarantees: Beyond Worst-Case Synthesis in Quantitative Games

Authors: Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin

Published in: LIPIcs, Volume 25, 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)

Abstract
Classical analysis of two-player quantitative games involves an adversary (modeling the environment of the system) which is purely antagonistic and asks for strict guarantees while Markov decision processes model systems facing a purely randomized environment: the aim is then to optimize the expected payoff, with no guarantee on individual outcomes. We introduce the beyond worst-case synthesis problem, which is to construct strategies that guarantee some quantitative requirement in the worst-case while providing an higher expected value against a particular stochastic model of the environment given as input. We consider both the mean-payoff value problem and the shortest path problem. In both cases, we show how to decide the existence of finite-memory strategies satisfying the problem and how to synthesize one if one exists. We establish algorithms and we study complexity bounds and memory requirements.
Cite as

Véronique Bruyère, Emmanuel Filiot, Mickael Randour, and Jean-François Raskin. Meet Your Expectations With Guarantees: Beyond Worst-Case Synthesis in Quantitative Games. In 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 25, pp. 199-213, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.STACS.2014.199,
  author =	{Bruy\`{e}re, V\'{e}ronique and Filiot, Emmanuel and Randour, Mickael and Raskin, Jean-Fran\c{c}ois},
  title =	{{Meet Your Expectations With Guarantees: Beyond Worst-Case Synthesis in Quantitative Games}},
  booktitle =	{31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)},
  pages =	{199--213},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-65-1},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{25},
  editor =	{Mayr, Ernst W. and Portier, Natacha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2014.199},
  URN =		{urn:nbn:de:0030-drops-44589},
  doi =		{10.4230/LIPIcs.STACS.2014.199},
  annote =	{Keywords: two-player games on graphs, Markov decision processes, quantitative objectives, synthesis, worst-case and expected value, mean-payoff, shortest path}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.505
Generalized Mean-payoff and Energy Games

Authors: Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Generalized mean-payoff and energy games replace individual weights by tuples, and the limit average (resp. running sum) of each coordinate must be (resp. remain) nonnegative. These games have applications in the synthesis of resource-bounded processes with multiple resources. We prove the finite-memory determinacy of generalized energy games and show the inter-reducibility of generalized mean-payoff and energy games for finite-memory strategies. We also improve the computational complexity for solving both classes of games with finite-memory strategies: while the previously best known upper bound was EXPSPACE, and no lower bound was known, we give an optimal coNP-complete bound. For memoryless strategies, we show that the problem of deciding the existence of a winning strategy for the protagonist is NP-complete.
Cite as

Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Generalized Mean-payoff and Energy Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 505-516, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.FSTTCS.2010.505,
  author =	{Chatterjee, Krishnendu and Doyen, Laurent and Henzinger, Thomas A. and Raskin, Jean-Fran\c{c}ois},
  title =	{{Generalized Mean-payoff and Energy Games}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{505--516},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.505},
  URN =		{urn:nbn:de:0030-drops-28484},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.505},
  annote =	{Keywords: mean-payoff games, energy games, finite memory strategies, determinacy}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact